%
% constraints.pro --- functions for producing mathematica code
%

%initialise(-PR,-RO): initialise assertions for given protocol and role
initialise(PR,RO) :-
  findall(M,protoknow(PR,RO,M),KB),assert(kb(KB)),       % kb: knowledge base
  xflatten(KB,KBF),assert(kbf(KBF)),                     % kbf: flattened knowledge base
  allmessages(SET),                                      % all messages of interest
  number(SET,TBL), assert(tbl(TBL)),                     % put in table
  celist(MAT),forall(member((X,Y),MAT),assert(ce(X,Y))). % precompute possible CEs

number([],_,[]).
number([X|LST],N,[(N,X)|RET]) :- NP1 is N+1, number(LST,NP1,RET).
number(LST,RET) :- number(LST,1,RET).

allmessages(SET) :-
  kb(KB),
  findall(M,(dblereq(KB,M,_),M\=pri(lst,_)),LST), list_to_set(LST,SET).

lookup(M,IX) :- tbl(TBL),member((IX,M),TBL),!.
lookup(M,_)  :- print('** Item not found: '),print(M),print('\n'),fail.

lookupfail(M,IX) :- tbl(TBL),member((IX,M),TBL).

% TODO: lookups and toindex seem to do the same thing???
lookups([],[]).
lookups([X|LST],[RX|RLST]) :- lookup(X,RX), lookups(LST,RLST).

toindex([],[]).
toindex([X|LST],[XP|LSTP]) :- toindex(X,XP), toindex(LST,LSTP).
toindex(M,IX) :- not(is_list(M)), lookup(M,IX).

celist([],_,[]).
celist([(IXP,MP)|LST],(IX,M),[(IX,IXP)|RET]) :- cecext(M,MP,_), !, celist(LST,(IX,M),RET).
celist([_|LST],(IX,M),RET) :- celist(LST,(IX,M),RET).

celist(MAT) :-
  tbl(TBL),findall(Z,(member((IX,M),TBL),celist(TBL,(IX,M),Z)),MATS),append(MATS,MAT).

% l2c :: [[msg]] -> constraint
li2c([],true) :- !.
li2c([X],X) :- !.
li2c(LST,and(LST)).
l2c([],false) :- !.
l2c([X],Y) :- li2c(X,Y), !.
l2c(LST,or(LSTP)) :- findall(I,(member(X,LST),li2c(X,I)),LSTP).

% ----- handling of boolean propositions: simplification, printing ------------

bsapply([],[]).
bsapply([X|LST],[XR|LSTR]) :- boolsimp(X,XR), bsapply(LST,LSTR).

boolsimp(or([]),false) :- !.
boolsimp(and([]),true) :- !.
boolsimp(or(LST),true) :- bsapply(LST,LSTP), member(true,LSTP), !.
boolsimp(and(LST),false) :- bsapply(LST,LSTP), member(false,LSTP), !.
boolsimp(or([X]),Y) :- boolsimp(X,Y), !.
boolsimp(and([X]),Y) :- boolsimp(X,Y), !.
boolsimp(and(X),and(XP)) :- bsapply(X,XP), !.
boolsimp(or(X),or(XP)) :- bsapply(X,XP), !.
boolsimp(X,X).

printorx([X]) :- !, printbool(X).
printorx([X|LST]) :- printbool(X), print('||'), printorx(LST).

printandx([X]) :- !, printbool(X).
printandx([X|LST]) :- printbool(X), print('&&'), printandx(LST).

printbool(true) :- print('True').
printbool(false) :- print('False').
printbool(X) :- number(X), print(X).
printbool(ce(X,Y)) :- print('ce['),print(X),print(','),print(Y),print(']').
printbool(or([])) :- !, printbool(false).
printbool(or([X])) :- !, printbool(X).
printbool(or(LST)) :- print('('), printorx(LST), print(')').
printbool(and([])) :- !, printbool(true).
printbool(and([X])) :- !, printbool(X).
printbool(and(LST)) :- print('('), printandx(LST), print(')').

% ----- compute construction path of message (proposition stating from what 
%       others it can be built ------------------------------------------------

constrpathmap([],[]).
constrpathmap([X|LST],[RX|RLST]) :- constrpath(X,RX), constrpathmap(LST,RLST).

constrpath1(IX,IX).
constrpath1(IX,and(LSTR)) :-
  lookup(M,IX), consneededsum(M,LST), xflatten(LST,LSTP), lookups(LSTP,IXS),
  constrpathmap(IXS,LSTR).
constrpath(IX,or(LST)) :-
  findall(CND,constrpath1(IX,CND),LSTP),
  list_to_set(LSTP,LST).

% ----- compute single elimination rules for deriving a given message (no
%       testing) --------------------------------------------------------------

elrules1(IX,[IXS,RET]) :-
  lookup(TAR,IX),
  tbl(MSGS),
  member((IXS,SRC),MSGS),
  eltestneededsum(SRC,TARP,REQS), 
  xflatten(TARP,TARPF),
  member(TAR,TARPF),
  xflatten(REQS,REQSP),
  not(member(TAR,REQSP)),           % no testing rules
  lookups(REQSP,RET).
elrules(IX,RET) :-
  findall(RULE,elrules1(IX,RULE),RULES),
  list_to_set(RULES,RET).

printelrule([IX,LST]) :-
  print('{'),print(IX),print(','),printbool(and(LST)),print('}').

printelrulesl([]).
printelrulesl([X]) :- !, printelrule(X).
printelrulesl([X|LST]) :- printelrule(X), print(','), printelrulesl(LST).

printelrules(IX) :-
  elrules(IX,RET),
  print('elrules['),print(IX),print(']={'),printelrulesl(RET),print('};\n').

% ----- compute complete elimination requirements for a given message,
%       including testing -----------------------------------------------------

resolve(M,REQS) :-
  kb(KB),findall(REQP,(dblereq(KB,M,REQ),xflatten(REQ,REQP)),REQSP),minimals(REQSP,REQS).

resolveix(IX,REQIXS) :-
  lookupfail(M,IX), resolve(M,REQS), toindex(REQS,REQIXS).

printeltestpaths(IX) :-
  resolveix(IX,RET0), l2c(RET0,RET1),
  print('eltestrules['),print(IX),print(']='),printbool(RET1),print(';\n').

% ----- print possible CEs ----------------------------------------------------

printces(IX) :-
  findall(Y,(ce(IX,Y),Y\=IX),YS),
  print('ces['),print(IX),print(']='),printbool(or(YS)),print(';\n').
